A, B:Realizer.
R-Feasible(A)  R-Feasible(B)  A || B  (i:Id. R-state(A;i) || R-state(B;i)) 

latex

Definitions

, t  T, {x:A| B(x) }, x:AB(x), #$n, a<b, Void, False, A, , R-state(R;i), ij, -n, n-m, R-size(R), n+m, R-ds(R;i), IdDeq, Type, Id, f || g, x:A. B(x), A || B, P  Q, R-Feasible(R), AB, Realizer, , es realizer ind Rplus compseq tag def, b, b, , s = t, Prop, Rplus?(x1), x:AB(x), P & Q, P  Q, {T}, SQType(T), s ~ t, left+right, P  Q, Rplus-right(x1), Rplus-left(x1), x.A(x), x. t(x), x:A. B(x), Top, es realizer ind Rnone compseq tag def, Rnone?(x1), a:A fp B(a), Rds(R), R-loc(R), a = b, Unit, , if b t else f fi, Atom$n, True, P  Q, T, EqDecider(T), f(a), x(s)

Lemmas

fpf-compatible wf, squash wf, true wf, deq wf, R-ds-Rds, Id sq, ifthenelse wf, fpf wf, fpf-empty wf, top wf, not functionality wrt iff, assert-eq-id, eq id wf, R-loc wf, Rds wf, fpf-empty-compatible-right, fpf-empty-compatible-left, fpf-trivial-subtype-top, Rnone? wf, Rnone-implies, fpf-compatible-join, R-Feasible-Rplus, R-size-decreases, fpf-compatible-join2, fpf-compatible-symmetry, id-deq wf, R-ds wf, Rplus-left wf, Rplus-right wf, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, Rplus? wf, bool wf, bnot wf, not wf, assert wf, Rplus-implies, ge wf, nat properties, nat wf, Id wf, R-compat wf, R-Feasible wf, es realizer wf, le wf, R-size wf, nat plus wf